plus2(plus2(X, Y), Z) -> plus2(X, plus2(Y, Z))
times2(X, s1(Y)) -> plus2(X, times2(Y, X))
↳ QTRS
↳ DependencyPairsProof
plus2(plus2(X, Y), Z) -> plus2(X, plus2(Y, Z))
times2(X, s1(Y)) -> plus2(X, times2(Y, X))
PLUS2(plus2(X, Y), Z) -> PLUS2(X, plus2(Y, Z))
PLUS2(plus2(X, Y), Z) -> PLUS2(Y, Z)
TIMES2(X, s1(Y)) -> TIMES2(Y, X)
TIMES2(X, s1(Y)) -> PLUS2(X, times2(Y, X))
plus2(plus2(X, Y), Z) -> plus2(X, plus2(Y, Z))
times2(X, s1(Y)) -> plus2(X, times2(Y, X))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
PLUS2(plus2(X, Y), Z) -> PLUS2(X, plus2(Y, Z))
PLUS2(plus2(X, Y), Z) -> PLUS2(Y, Z)
TIMES2(X, s1(Y)) -> TIMES2(Y, X)
TIMES2(X, s1(Y)) -> PLUS2(X, times2(Y, X))
plus2(plus2(X, Y), Z) -> plus2(X, plus2(Y, Z))
times2(X, s1(Y)) -> plus2(X, times2(Y, X))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
PLUS2(plus2(X, Y), Z) -> PLUS2(X, plus2(Y, Z))
PLUS2(plus2(X, Y), Z) -> PLUS2(Y, Z)
plus2(plus2(X, Y), Z) -> plus2(X, plus2(Y, Z))
times2(X, s1(Y)) -> plus2(X, times2(Y, X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PLUS2(plus2(X, Y), Z) -> PLUS2(X, plus2(Y, Z))
PLUS2(plus2(X, Y), Z) -> PLUS2(Y, Z)
POL( PLUS2(x1, x2) ) = max{0, x1 - 2}
POL( plus2(x1, x2) ) = x1 + x2 + 3
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
plus2(plus2(X, Y), Z) -> plus2(X, plus2(Y, Z))
times2(X, s1(Y)) -> plus2(X, times2(Y, X))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
TIMES2(X, s1(Y)) -> TIMES2(Y, X)
plus2(plus2(X, Y), Z) -> plus2(X, plus2(Y, Z))
times2(X, s1(Y)) -> plus2(X, times2(Y, X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
TIMES2(X, s1(Y)) -> TIMES2(Y, X)
POL( TIMES2(x1, x2) ) = max{0, x1 + x2 - 2}
POL( s1(x1) ) = x1 + 3
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
plus2(plus2(X, Y), Z) -> plus2(X, plus2(Y, Z))
times2(X, s1(Y)) -> plus2(X, times2(Y, X))